# To change this template, choose Tools | Templates
# and open the template in the editor.
$LOAD_PATH.unshift File.join(File.dirname(__FILE__),'../../..','ext_pr1/lib')
require 'ext_pr1_v4'



#typdefinitionen für 1d objekte
def point1dim?(coord) coord.int? end
def range1dim?(first, last) first.point1d? and last.point1d? and  first.coord <= last.coord  end
def union1dim?(left, right) shape1dim?(left) and shape1dim?(right)    end
def shape1dim?(val)          val.range1d? or val.union1d?       end


#typprädikate für 2d objekte
def point2dim?(p1,p2)     p1.point1d? and p2.point1d?          end
def range2dim?(r1,r2)    r1.range1d? and r2.range1d?           end
def union2dim?(left,right) shape2dim?(left) and shape2dim?(right)    end
def shape2dim?(s1) s1.range2d? or s1.union2d? end

#gemeinsame typprädikate
def point?(val) val.point1d? or val.point2d? end
def prim_shape?(val) val.range1d? or val.range2d? end
def union_shape?(val) val.union1d? or val.union2d? end
def shape?(val) prim_shape?(val) or union_shape?(val) end
def graph_obj?(val) point?(val) or shape?(val) end

#1D KLASSEN

#1 dimensionaler punkt
#def range1d?(range) 
#Point1d ::= :Point1d[:x] :: x = Int
def_class(:Point1d,[:coord]) {
  def invariant?
    point1dim?(coord) 
  end
}
#1 dimensionales intervall mit 1 dimensionalen punkten
#Range1d ::= :Range[:first,:last] :: first, last :: first, last == :Point1d
def_class(:Range1d,[:first, :last]) {
  def invariant?
  range1dim?(first, last)
  end
}

#Union1d als Vereinigung von 2 Shape1d
#Union1d ::= :Union1d[:shape1, :shape2] :: shape1, shape2 :: shape1, shape2 == :Shape1d

def_class(:Union1d,[:left, :right]) {
  def invariant?
   union1dim?(left, right)
  end
}

#Shape1d als Überbegriff für Union1d und Range1d
#:Shape1d ::= :Shape1d[:shape] :: shape :: shape == :Range1d or shape == Union1d

#def_class(:Shape1d,[:shape]) {
#  def invariant? 
#    shape1dim?(shape)
#  end 
#}


#2D KLASSEN

#2d punkt als kreuzprodukt aus 2 Point1d
# :Point2d ::= :Point2d[x,y] :: x, y :: x,y == :Point1d

def_class(:Point2d,[:x, :y]) {
  def invariant?
    point2dim?(x,y)
  end
  
}

#2d range als kreuzprodukt aus 2 Range1d
# :Range2d ::= :Range2d[range_x, range_y] :: range_x, range_y :: range_x, range_y == Range1d

def_class(:Range2d,[:range_x, :range_y]) {
  def invariant?
    range2dim?(range_x, range_y)
  end
}

#2d union als vereinigung von 2 shapes
# :Union2d ::= :Union[:left,:right] :: left, right :: left, right == Shape2d

def_class(:Union2d,[:left, :right]) {
  def invariant?
    union2dim?(left, right)
  end
}  
#2d Shape als Überbegriff für Union2d und Range2d
#:Shape2d ::= :Shape2d[:shape1, shape2] :: shape1, shape2 :: shape1, shape2 == (:Range2d or Union2d)
#def_class(:Shape2d,[:shape1, :shape2]) {
#  def invariant?
#    shape2dim?(shape1, shape2)
#  end
#}

#Translationsfunktion für 1d-Formen
# translate1d ::= shape, point :: (Union1d || Range1d) x Point ->? (Union1d || Range1d) ::
#test(translate1d(Range1d[Point1d[1],Point1d[2]], Point1d[2]) => Range1d[Point1d[3],Point1d[4]],
#translate1d(Union1d[Range1d[Point1d[1],Point1d[2]], Range1d[Point1d[2],Point1d[4]]], Point1d[2]) => Union1d[Range1d[Point1d[3],Point1d[4]], Range1d[Point1d[4],Point1d[6]]],
#translate1d(Union1d[Range1d[1,2], Union1d[Range1d[3,5],Range1d[2,4]], Point1d[2]]) => Union1d[Range1d[3,4],Union1d[Range1d[5,7],Range1d[4,6]]
#translate1d(Range1d["a",4], Point1d[2]) => Err
#translate1d(Range1d[1,2], 3) => Err
#translate1d(Range1d[Point1d[2], Point1d[1]], Point1d[3]) => Err

            #hilfsfunktion auf 0 dimensionen
            #translate0d ::= p1, p2 :: Point x Point ->? Point ::
            #test(translate0d(Point1d[1], Point1d[2]) => Point1d[3]
            #translate0d(Point1d[2], [1]) => Err, translate0d([1], Point1d[2]) => Err

            def translate0d(p1, p2)
              check_pre((p1.point1d? and p2.point1d?))
              Point1d[(p1.coord + p2.coord)]
            end
            
            
def translate1d(shape, point)
  check_pre((shape1dim?(shape) and point.point1d?))
  if shape.range1d? then Range1d[translate0d(shape.first, point), translate0d(shape.last, point)]
  elsif shape.union1d? then Union1d[translate1d(shape.left, point), translate1d(shape.right, point)]
  
  end
end

#Translationsfunktion für 2d-Formen
# translate2d ::= shape, point :: (Union2d || Range2d) x Point2d ->? (Union2d || Range2d) ::
# test(Range2d[Range1d[P1,P2], Range1d[P2,P3]], Point2d[1,2]) => Range2d[Range1d[P2,P3], Range1d[P4,P5]],
# translate2d(Union2d[Range2d[Range1d[P1,P1],Range1d[P1,P1]], Union2d[Range2d[Range1d[P1,P1],Range1d[P1,P1]],Range2d[Range1d[P1,P1],Range1d[P1,P1]]]], Point2d[P1,P2])
# => Union2d[Range2d[Range1d[P2,P2],Range1d[P3,P3´]], Union2d[Range2d[Range1d[P2,P2],Range1d[P3,P3]],Range2d[Range1d[P2,P2],Range1d[P3,P3]]]]
#
def translate2d(shape, point)
  check_pre((shape2dim?(shape) and point.point2d?))
  if shape.range2d? then Range2d[translate1d(shape.range_x, point.x), translate1d(shape.range_y, point.y)]
  elsif shape.union2d? then Union2d[translate2d(shape.left, point), translate2d(shape.right, point)]
  end
end
  
#translate
#Translationsfunktion für beliebige Formen
#translate ::= shape, point :: (Union1d || Range1d || Union || Range) x Point ->? (Union1d || Range1d || Union2d || Range2d)
#test(translate(Range1d[Point1d[1],Point1d[2]], Point1d[2]) => Range1d[Point1d[3],Point1d[4]],
#translate(Union1d[Range1d[Point1d[1],Point1d[2]], Range1d[Point1d[2],Point1d[4]]], Point1d[2]) => Union1d[Range1d[Point1d[3],Point1d[4]], Range1d[Point1d[4],Point1d[6]]],
#translate(Union1d[Range1d[1,2], Union1d[Range1d[3,5],Range1d[2,4]], Point1d[2]]) => Union1d[Range1d[3,4],Union1d[Range1d[5,7],Range1d[4,6]]
#(Range2d[Range1d[P1,P2], Range1d[P2,P3]], Point2d[1,2]) => Range2d[Range1d[P2,P3], Range1d[P4,P5]],
# translate(Union2d[Range2d[Range1d[P1,P1],Range1d[P1,P1]], Union2d[Range2d[Range1d[P1,P1],Range1d[P1,P1]],Range2d[Range1d[P1,P1],Range1d[P1,P1]]]], Point2d[P1,P2])
# => Union2d[Range2d[Range1d[P2,P2],Range1d[P3,P3´]], Union2d[Range2d[Range1d[P2,P2],Range1d[P3,P3]],Range2d[Range1d[P2,P2],Range1d[P3,P3]]]],
#translate(Range2d[Range1d[P1,P1], Range1d[P1,P1]], Point1d[1]) = > Err,
#translate(Range1d[P1,P3], 4) => Err)

def translate(shape, point)
check_pre((shape?(shape) and point?(point)))
if (shape1dim?(shape) and point.point1d?) then translate1d(shape, point)
elsif (shape2dim?(shape) and point.point2d?) then translate2d(shape, point)
else check_pre(false)
end 
end 

#bounds
#Vereiningung von zwei Formen
#bounds ::= (shape) :: shape -> (range1d || range2d)
#test (bounds[Range1d[P1,P2]]) => Range1d[P1,P2]
#bounds([Range2d[Range1d[P1,P2], Range1d[P2,P3]]) => Range2d[Range1d[P1,P2], Range1d[P2,P3]]
#bounds(Union1d[Range1d[P1,P2],Range1d[P2,P3]]) => Range1d[P1,P3],
#bounds(Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P3]],Range2d[Range1d[P2,P3],Range1d[P3,P4]]]) => Range2d[Range1d[P1,P3],Range1d[P2,P4]],
#bounds(Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P3]],Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P3]],Range2d[Range1d[P2,P3],Range1d[P3,P4]]]]) 
#=> Range2d[Range1d[P1,P3],Range1d[P2,P4]]
#bounds(Point1d[1]) => Err

    #Bounding-Range
    #Bildet die Länge vom niedrigsten zum längesten Punkt
    #bounding_range ::= (r1,r2) ::  (range1d x range1d) -> range1d ||
    #                               (range2d x range2d) -> range2d
    #tests (bounding_range(Range1d[P1,P2], Range1d[P2,P3]) => Range1d[P1,P3],
    #bounding_range(Range2d[Range1d[P1,P2],Range1d[P2,P3]], Range2d[Range1d[P3,P4],Range1d[P4,P5]]) => Range2d[Range1d[P1,P4],Range1d[P2,P5]],
    #bounding_range(Range1d[P1,P2],Range2d[Range1d[P1,P2],Range1d[P2,P3]]) => Err,
    #bounding_range(Range1d[P1,P2], 4) => Err
  

    def bounding_range(r1, r2)
    check_pre((prim_shape?(r1) and prim_shape?(r2)))
    if (r1.range1d? and r2.range1d?) then Range1d[Point1d[r1.first.coord.min(r2.first.coord)],Point1d[r1.last.coord.max(r2.last.coord)]]
    elsif (r1.range2d? and r2.range2d?) then Range2d[bounding_range(r1.range_x,r2.range_x),bounding_range(r1.range_y,r2.range_y)]
    else check_pre(false)
    end
    end
    
def bounds(shape)
  check_pre((shape?(shape)))
  if union_shape?(shape) then bounding_range(bounds(shape.left),bounds(shape.right))
  elsif prim_shape?(shape) then shape
  else check_pre(false)
  end
end


#graph_equal?
#Ermittlung ob zwei Grafiken mit der gleichen Formel erzeugt wurden
#graph_equal? ::= (o1,o2) :: GraphObj x GraphObj -> Bool
#test graph_equal?(P1, P1) => true
#(graph_equal?(Point2d[P1,P2], Point2d[P1,P2])) => true
#(graph_equal?(Range1d[P1,P2], Range1d[P1,P2])) => true
#(graph_equal?(Range2d[Range1d[P1,P2], Range1d[P1,P2]], Range2d[Range1d[P1,P2], Range1d[P1,P2]])) => true
#(graph_equal?(Union1d[Range1d[P1,P2],Range1d[P2,P3]], Union1d[Range1d[P1,P2],Range1d[P2,P3]])) => true
#(graph_equal?(Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P3]], Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P3]])) => true
#(graph_equal?(P1,P2)) => false
#(graph_equal?(Point2d[P1,P2], Point2d[P1,P2])) => false
#(graph_equal?(Range1d[P1,P2], Range1d[P2,P3])) => false
#(graph_equal?(Range2d[Range1d[P1,P2], Range1d[P1,P2]], Range2d[Range1d[P2,P3], Range1d[P1,P2]])) => false 
#(graph_equal?(Union1d[Range1d[P1,P2],Range1d[P2,P3]], Union1d[Range1d[P1,P2],Range1d[P2,P4]])) => false
#(graph_equal?(Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P3]], Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P4]])) => false

  def graph_equal_?(o1, o2)
   if point?(o1) and point?(o2) then
     if o1.point1d? and o2.point1d? then o1.coord == o2.coord 
     elsif o1.point2d? and o2.point2d? then (graph_equal_?(o1.x, o2.x) and graph_equal_?(o1.y, o2.y))
     else false
     end
   elsif union_shape?(o1) and union_shape?(o2) then (graph_equal?(o1.left, o2.left) and graph_equal?(o1.right, o2.right))
   elsif prim_shape?(o1) and prim_shape?(o2) then
     if o1.range1d? and o2.range1d? then (graph_equal?(o1.first, o2.first) and graph_equal?(o1.last, o2.last))
     elsif o1.range2d? and o2.range2d? then (graph_equal?(o1.range_x, o2.range_x) and graph_equal?(o1.range_y, o2.range_y)) 
     else false
     end
   end
  
  end
  
  def graph_equal?(o1,o2)
     check_pre((graph_obj?(o1) and graph_obj?(o2)))
     graph_equal_?(o1, o2)
     
  end
  
  #graph_equal_trans?
  #Ermittlung, ob die Form von zwei Grafiken gleich ist
  #graph_equal_trans? ::= (o1,o2) :: Any x Any ->? Bool
  #test(graph_equal_trans?(P1,P2)) => true
  #graph_equal_trans?(Point2d[P1,P2], Point2d[P3,P4])) => true
  #graph_equal_trans?(Range1d[P1,P2], Range1d[P3,P4])) => true
  #graph_equal_trans?(Range2d[Range1d[P1,P2], Range1d[P1,P2]], Range2d[Range1d[P3,P4], Range1d[P3,P4]])) => true
  #graph_equal_trans?(Union1d[Range1d[P1,P2],Range1d[P2,P3]], Union1d[Range1d[P2,P3],Range1d[P3,P4]])) => true
  #graph_equal_trans?(Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P3]], Range2d[Range1d[P1,P2],Range1d[P2,P3]]], Union2d[Range2d[Range1d[P2,P3],Range1d[P3,P4]], Range2d[Range1d[P2,P3],Range1d[P3,P4]]])) => true
  #graph_equal_trans?(Range1d[P1,P2], Range1d[P2,P4])) => false
  #graph_equal_trans?(Range2d[Range1d[P1,P2], Range1d[P1,P2]], Range2d[Range1d[P3,P4], Range1d[P3,P5]])) => false 
  #graph_equal_trans?(Union1d[Range1d[P1,P2],Range1d[P2,P3]], Union1d[Range1d[P2,P4],Range1d[P3,P5]])) => false
  #graph_equal_trans?(Union2d[Range2d[Range1d[P1,P2],Range1d[P2,P3]], Range2d[Range1d[P1,P2],Range1d[P2,P3]]], Union2d[Range2d[Range1d[P2,P4],Range1d[P3,P5]], Range2d[Range1d[P2,P4],Range1d[P3,P5]]])) => false
  #graph_equal?("a","a")) => Err
  #graph_equal?(P1,"a")) => Err
  #graph_equal?("a",P1)) => Err

  def graph_equal_trans?(o1,o2)
      check_pre((graph_obj?(o1) and graph_obj?(o2)))
     if shape1dim?(o1) and shape1dim?(o2) then 
       to1 = translate(o1, Point1d[(bounds(o2).first.coord - bounds(o1).first.coord)])
     elsif shape2dim?(o1) and shape2dim?(o2) then
       to1 = translate(o1, Point2d[Point1d[(bounds(o2).range_x.first.coord - bounds(o1).range_x.first.coord)], Point1d[(bounds(o2).range_y.first.coord - bounds(o1).range_y.first.coord)]])
     elsif o1.point1d? and o2.point1d? then 
       to1 = Point1d[o1.coord + (o2.coord - o1.coord)]
     elsif o1.point2d? and o2.point2d? then
       to1 = Point2d[Point1d[o1.x.coord + (o2.x.coord - o1.x.coord)], Point1d[o1.y.coord + (o2.y.coord - o1.y.coord)]]
    end
     
    graph_equal?(to1, o2)
  end
  
  #in?
  #funktion, die testet, ob ein Punkt in einer Form liegt
  #in? ::= (point, shape) :: Point x Shape -> Bool
  #test(in?(P2,Range1d[P1,P2]) => true,
  #in?(P2, Union1d[Range1d[P1, P2], Range1d[P2, P3]]) => true,
  #in?(P3, Union1d[Range1d[P1, P2], Range1d[P4, P5]]) => false,
  #in?(Point2d[P2,P2], Range2d[Range1d[P0, P4], Range1d[P2, P4]]) => true,
  #in?(Point2d[P2,P2], Union2d[Range2d[Range1d[P0, P4], Range1d[P2, P4]], Range2d[Range1d[P1, P5], Range1d[P3, P5]]]) => true,
  #in?(Point2d[P2,P2], Union2d[Range2d[Range1d[P0, P02], Range1d[P0, P1]], Range2d[Range1d[P2, P3], Range1d[P3, P5]]]) => false,
  #in?(P1, Range2d[Range2d[Range1d[P0, P4], Range1d[P2, P4]]]) => Err,
  #in?(Point2d[P2,P2], Range1d[P1,P2]) => Err
  #in?(P1, "1") => Err
  #in? ("1", Range1d[P1, P2]) => Err
  
  def in?(point, shape)
    check_pre((point?(point) and shape?(shape)))
    if prim_shape?(shape) then include?(point, shape)
    elsif union_shape?(shape) then (in?(point, shape.left) or in?(point, shape.right))
    else false
    end
  end
  
          #hilfsfunktion inlude1dim?, die nur zahlen vergleicht und einen wahrheitswert liefert
          #include1dim? ::= (coord, first, last) :: Int x Int x Int -> Bool
        
          def include1dim?(coord, first, last)
         ((first <= coord) and (coord <= last))
          end
     
      #Hilfsfunktion include? die prüft ob ein Punkt in einem Range enthalten ist
      #include? ::= (point, range) :: Point x Range -> Bool
      def include?(point, range)
        if point.point1d? and range.range1d? then include1dim?(point.coord, range.first.coord, range.last.coord)
        elsif point.point2d? and range.range2d? then (include1dim?(point.x.coord, range.range_x.first.coord, range.range_x.last.coord) and include1dim?(point.y.coord, range.range_y.first.coord, range.range_y.last.coord))
        else check_pre(false)
        end
      
      end